COMMENT ⊗   VALID 00003 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	%elepha.l[f89,jmc]	A try a the reservation program in logic
C00009 00003	\smallskip\centerline{Copyright \copyright\ 1989\ by John McCarthy}
C00010 ENDMK
C⊗;
%elepha.l[f89,jmc]	A try a the reservation program in logic
\input memo.tex[let,jmc]
\title{This is the key part needed to make the paper distributable.}
\section{Elephant Programs as Sentences of Logic}


 $$\eqalign{(∀psgr flt t)&(input t = request make commitment admit(psgr flt)\cr
	&\quad\quad ∧ ¬ holds(t,full flt)\cr
&⊃ (∃ seat) (holds(t,available(seat,flt)) ∧\cr
&\quad arises(t, commitment admit(psgr,flt, seat))\cr
	&\quad ∧ outputs(t,promise admit(psgr,flt,seat)))).\cr}$$

Note the use of $admit$ first with two argments and later with three.
We suppose that $admit$ actually has a large set of arguments with
default values.  When an $admit(\ldots )$ expression is encountered,
it is made obvious which arguments are being given values by the
expression and which get default values.  The signals for this are
the name of the variable or an actual named argment as in Common
Lisp.  The compiler will have to come up with a way of assigning
a seat from those available.

$$\eqalign{
(∀psgr flt t) &(input t = query exists commitment admit(psgr flt)\cr
&⊃ outputs(t,if exists(t, commitment admit(psgr flt)) then\cr
&confirm(commitment admit(psgr flt seat)) else deny(input t))\cr}$$

$$\eqalign{
(∀psgr flt t) &(input t = request cancel commitment admit(psgr,flt)\cr
&⊃ revoke(t,commitment admit(psgr,flt))\cr}$$

$$\eqalign{
(∀t x)(&exists(t,commitment x) ≡ (∃t')(t' < t ∧ arises(t, commitment x))\cr & ∧
(∀t'')(t' < t'' < t ⊃ ¬revoke(t, commitment x)))\cr}$$

$$\eqalign{
(∀psgr flt t) &(input t = request admit(psgr,flt)\cr & ⊃
if exists(t, commitment admit( psgr,flt)\cr &\quad\quad then outputs(t,
command(agent,admit(psgr,flt,seat))\cr &\quad \quad else outputs(t, command(agent,
don't admit (psgr,flt))))\cr}$$

	Asserting that certain outputs occur and that certain propositions
hold doesn't establish that others don't occur.   Therefore, the program
as given is to be supplemented by circumscribing certain predicates,
namely $arises$, $outputs$ and $revoke$.

Remarks:

	1. Proving that a program fulfills its commitments
seems to be just a matter of expressing a commitment as making
sure a certain sentence is true, e.g. that the passenger is
allowed on the airplane.  In that case, proving that the program
fulfills its commitments is just a matter of showing that the
sentences expressing the commitments follow from the sentence
expressing the program.  The problem now is to decide what
class of sentences to allow as expressing various kinds of
commitments.  If the commitments are to be externally
expressed as promises, then they have to belong to the
i-o language.

	2. Commitments are like specifications, but they are
to be considered as dynamic, i.e. specific commitments are
created as the program runs.  We can ask what are the
program's commitments when it is in a given state.  Indeed
we might even be able to ask the program what its commitments
are.

	3. An Elephant interpreter need only match the inputs
against the program statements with inputs as premisses.  It then
issues the outputs, performs the actions and asserts the other
conclusions of the statement.  The circumscriptions should not
have to be consulted, because they can be regarded as asserting
that the only events that occur are those specified in the
statements.  Here the situation is similar to that of logic
programming.  The circumscriptions {\it are} used in proving that
the program meets its specifications, e.g. fulfills its commitments.

	There is a theorem about this that remains to be
precisely formulated and then proved.  Making it provable
might involve some revisions of the formalism.

\noindent Vladimir's message

Maybe you don't need $holds$ at all. You can use these abbreviations instead:

$$available(t,seat,flt) ≡ ¬∃psgr exists(t,commitment admit(psgr,flt,seat)),$$
$$full(t,flt) ≡ ¬∃seat available(t,seat,flt).$$

\smallskip\centerline{Copyright \copyright\ 1989\ by John McCarthy}
\smallskip\noindent{\fiverm This draft of elepha.l[f89,JMC]\ TEXed on \jmcdate\ at \theTime}
%File originated on 28-Nov-89
\vfill\eject\end